es:ES, T:Type, x:Id, e1, e2:{e:E| @loc(e)(x:T)} , P:(T).
e[e1,e2).P((x after e))  e(e1,e2].P(x when e) 

latex

Definitions	P  Q, (e <loc e'), e loc e' , True, T, (discrete state when e), (discrete state after e), P  Q, P & Q, P  Q, ff, tt, P  Q, if b then t else f fi , x. t(x), t  T, discrete state@i, e(e1,e2].P(e), e[e1,e2).P(e), , x:A. B(x), {T}, SQType(T), SqStable(P), Unit, , False, A, @i(x:T), x(s),
Lemmas	es-causl wf, es-le-loc, es-when wf, Id sq, decidable assert, sq stable from decidable, es-after wf, es-le wf, es-locl wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, assert wf, bool wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-E wf, top wf, es-vartype wf, es-isconst wf, ifthenelse wf, alle-between1-after